Nuprl Definition : discrete_struct
0,22
postcript
pdf
DS(
A
) ==
sort
:(
A
Type)
(
a
:
A
EqDecider(
sort
(
a
)))
latex
clarification:
discrete_struct{i:l}(
A
) ==
sort
:(
A
Type{i})
(
a
:
A
EqDecider(
sort
(
a
)))
latex
Definitions
EqDecider(
T
)
FDL editor aliases
DS
origin
Type)
(a:AEqDecider(sort(a)))
Type{i})(a:AEqDecider(sort(a))) Type)(a:AEqDecider(sort(a)))
Type{i})(a:AEqDecider(sort(a)))